\section{Approach\Comment{Technique}}

Figure~\ref{fig:approach} illustrates the approach of \tname{} to
report race warnings.  Consider that a program model checker produces
two schedules ``sched.1'' and ``sched.2'' for the subject under
test.  The figure shows these scheduling with vertical lines.  The
small rectangles over the lines denote context switches in each
schedule and the line segments between rectangles denote straight-line
execution within individual threads according to an interleaving
semantics of execution.  The approach used by \tname{} is to monitor
\emph{distinct} accesses to the memory and to analyze this information
on-the-fly.  It stores access-related information per object and per
field.  In this scenario, \tname{} is able to identify that accesses
a1 and a2 observed with different schedules are conflicting (see box
\label{sec:approach}
\begin{wrapfigure}{r}{0.54\textwidth}
  \vspace{-5ex}
  \centering
  \includegraphics[scale=0.6]{figures/approach.eps}
  \caption{\label{fig:approach}Conceptual illustration of \tname{}.}
  \vspace{-3ex}
\end{wrapfigure}
 note).  Conceptually, it speculates that it would be possible to
create a scheduling combining the two straight-line blocks of
execution.  On the one hand, note that the model checker may need to
produce a combinatorial number of other schedules before exercising
one with such potential racy combination.  On the other hand, note
that such combination that \tname{} created may not actually occur due
to the causal dependencies that may exist (and we do not track)
associated with the execution of a1 or a2 (see
Section~\ref{sec:limitations}).\Comment{ The hypothesis of \tname{} is
  that lack of awareness of causal dependencies will not play}

%%\vspace{1ex}\noindent\textbf{Monitoring.}  

\subsection{Online prediction}
\label{sec:monitoring}

\tname{} uses the \jpf{} infrastructure to observe relevant events
across state-space exploration.  We implemented \tname{} with a
bytecode listener, which receives notification instructions that can
modify heap or static area, namely the bytecode instructions
\CodeIn{PUTFIELD}, \CodeIn{GETFIELD}, \CodeIn{PUTSTATIC}, and
\CodeIn{GETSTATIC}.  We use two data-structures to store analysis
data.  The first stores memory access information; it is the raw data
for our analysis.  The other data-structure stores information about
the potential conflicts observed up to a given moment in the search;
this information is obtained from the raw data.  \tname{} checks if a
new memory access that the model checker notifies to the listener
represents potential race; it compares the new observation with
historical data.

Consider, for example, that \tname{} receives a notification of a new
write access to the field $o.f$ through the thread $t$ and lockset
$\mathit{ls}$.\Comment{ The tuple the
  $\langle{}W,o,f,t',\mathit{ls'}\rangle$ denotes such observation.}
\tname{} realizes that the raw data includes a tuple
$\langle{}R,o,f,t,\mathit{ls}\rangle$ indicating that a read access to
the same field realized by different threads ($t \neq t'$) and
disjoint locksets ($\mathit{ls} \cap \mathit{ls'}=\emptyset$) has been
observed previously.  In this case, \tname{} updates the second
data-structure with information about such potential conflict.  Note
that we relate the memory access observed during the search with the
historical information of memory accesses (i.e., accesses seen along
the current path or seen in other paths).  Even though cost is
proportional to the number of memory accesses, we only compare
accesses to the same memory locations.  Note that \jpf{} implements a
race \emph{detector} based on the Eraser
algorithm~\cite{savage-etal-1997} but the race \emph{predictor} of
\tname{} does not build on that.  While a race detector considers only
one execution path, \tname{} considers many paths using the history of
memory accesses.

\tname{} filters similar detected conflicts.  For example, we observed
that several of conflicting accesses initially reported in our
experiments where symmetric with respect to the threads involved.  The
access pattern was the same, but the threads involved in the
manifestation of the race were different.  In such cases, we report
only one representative of the symmetry class, significantly reducing
the number of reported warnings.


\subsection{Limitations}
\label{sec:limitations}
%% \tname{}'s goal is to complement model checking with earlier feedback.
%% The approach is lightweight and non-intrusive with respect to the
%% model checker behavior. 

We describe below key limitations of \tname{}.

\vspace{1ex}\noindent\textbf{Object ids.}  \tname{} correlates objects
involved across different exploration paths of the program.
Unfortunately, stateful model checkers, Java PathFinder particularly,
sometimes are not able to keep the identifier of the objects fixed
during exploration~\cite{lerda:01}.  The code below illustrates
this.\Comment{ characteristic.}

\small
\begin{verbatim}
  String s = "a"; if (Verify.getBoolean()) { s = "b"; /*<= comment*/ }
  Object x = new Object(); System.out.println(x);
\end{verbatim}
\normalsize

In this fragment, the JPF-provided \CodeIn{Verify.getBoolean()}
library call creates a non-deterministic choice, effectively forking
the execution path in two.  \jpf{} is unable to identify that the
objects assigned to variable \CodeIn{x} across both paths are in fact
the same.  That happens because in one of the branches execution
creates (and assigns) the string \CodeIn{``b''} (to variable
\CodeIn{s}) and
\begin{wrapfigure}{r}{0.57\textwidth}
  \vspace{-5ex}
  \centering
  \small

  \lstset{escapeinside={\%*}{*)}}
  \lstinputlisting[language=java,basicstyle=\scriptsize]{AlarmClock.java}


  \vspace{-2ex}
  \caption{\label{fig:causality}Fragment from \texttt{alarmclock}
    subject.  \tname{} reports a conflict in the read-write accesses
    to \texttt{id} even though they are causally dependent.}
  \vspace{-5ex}
\end{wrapfigure}
\normalsize
this changes the way \jpf{} assigns ids to objects.  The possibility
of using different ids for the same objects could lead to race misses
due to the inability of \tname{} to correlate memory accesses.
However, note that \jpf{} will use the same identity for one object
across all paths created from choices that follow the creation of that
object.

\vspace{1ex}\noindent\textbf{Causality.}  \tname{} does not detect
causally dependent memory accesses, which by definition cannot result
in races.  Figure~\ref{fig:causality} illustrates one scenario that
\tname{} reports a false positive for this reason.  The fragment is
extracted and simplified from the \CodeIn{alarmclock} subject.
\tname{} reports such false positive very early in the search ($<$5s).
In this example, the main function creates a \CodeIn{Client} object
and initializes the field \CodeIn{id} in the context of one (main)
thread, then it spawns the thread associated with the client object.
The method \CodeIn{run} reads the field \CodeIn{id} in the context of
the client thread.  The field \CodeIn{id} is not protected by any lock
but this is not the problem.  The figure shows, as comments, the
vector clocks associated with each access~\cite{lamport1978}.  Each
element of the vector corresponds to a counter associated with each
thread.  Note from the values of the vectors that the read access to
the field is causally dependent on the store access and could not
result in a race.


% LocalWords:  schedules sched Fnote bytecode PUTFIELD GETFIELD PUTSTATIC JPF
% LocalWords:  GETSTATIC lockset tuple locksets stateful PathFinder getBoolean
% LocalWords:  alarmclock Online escapeinside basicstyle AlarmClock
